(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source | Stéphane Graham-Lengrand, Basic example #1 from SMT'2017 preliminary repoprt |)
(set-info :category "crafted")
(set-info :status sat)
(declare-fun x1 () (_ BitVec 12))
(declare-fun x2 () (_ BitVec 12))
(declare-fun y () (_ BitVec 12))
(assert (= x2 (bvnot x1)))
(assert (= (concat ((_ extract 3 0) x1) ((_ extract 7 4) x2)) (concat ((_ extract 11 8) y) ((_ extract 11 8) y))))
(check-sat)
(exit)
